/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRK30
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ H


␈↓ ↓H␈↓α␈↓ α$REPRESENTATION OF RECURSIVE PROGRAMS IN FIRST ORDER LOGIC

␈↓ ↓H␈↓␈↓ α_This␈αpaper␈αpresents␈αmethods␈αof␈αrepresenting␈αrecursive␈αprograms␈αby␈αsentences␈αand␈αschemata
␈↓ ↓H␈↓of␈α
first␈α
order␈α
logic,␈α
characterization␈α
of␈α
␈↓↓recursion␈α
induction␈↓,␈α
␈↓↓subgoal␈α
induction␈↓,␈α∞␈↓↓inductive␈α
assertions␈↓
␈↓ ↓H␈↓and␈α⊂other␈α⊂ways␈α⊂of␈α⊂proving␈α⊂facts␈α⊂about␈α⊂programs␈α⊂as␈α⊂axiom␈α⊂schemata␈α⊂of␈α⊂first␈α⊂order␈α⊂logic,␈α∂and
␈↓ ↓H␈↓applications of these results to proving assertions about programs.


␈↓ ↓H␈↓α1. Introduction and Motivation.

␈↓ ↓H␈↓␈↓ α_It␈α
has␈αbeen␈α
concluded␈αfrom␈α
the␈α
undecideability␈αof␈α
both␈αequivalence␈α
and␈αnon-equivalence␈α
of
␈↓ ↓H␈↓abstract␈α⊃recursive␈α⊃program␈α⊃schemata␈α⊃that␈α⊃recursive␈α⊃programs␈α⊃cannot␈α⊃be␈α⊃characterized␈α⊃in␈α⊂first
␈↓ ↓H␈↓order␈α⊂logic.␈α⊃ Cooper␈α⊂(1969)␈α⊂showed␈α⊃how␈α⊂to␈α⊂characterize␈α⊃them␈α⊂in␈α⊂second␈α⊃order␈α⊂logic,␈α⊃and␈α⊂that
␈↓ ↓H␈↓seemed␈α∪to␈α∩settle␈α∪the␈α∪matter.␈α∩ However,␈α∪we␈α∩will␈α∪exhibit␈α∪first␈α∩order␈α∪characterizations␈α∪that␈α∩are
␈↓ ↓H␈↓incomplete␈α∞only␈α∞in␈α∞that␈α∞they␈α∞admit␈α∞non-standard␈α∞models␈α∞like␈α∞those␈α∞of␈α∞first␈α∞order␈α∞arithmetic.␈α
 It
␈↓ ↓H␈↓now␈αseems␈αlikely␈αthat␈αall␈α"ordinary"␈αassertions␈αabout␈αprograms␈αwill␈αbe␈αprovable␈αor␈αdisprovable␈αin
␈↓ ↓H␈↓first order theories.

␈↓ ↓H␈↓␈↓ α_Beyond␈α∂illuminating␈α∂the␈α⊂logical␈α∂structure␈α∂of␈α∂computer␈α⊂programs,␈α∂these␈α∂results␈α⊂have␈α∂some
␈↓ ↓H␈↓practical␈α∂significance.␈α∂ First,␈α∂correctness␈α∂of␈α⊂computer␈α∂programs␈α∂often␈α∂involves␈α∂facts␈α⊂about␈α∂other
␈↓ ↓H␈↓mathematical␈αdomains,␈α
and␈αthese␈αare␈α
often␈αconveniently␈αexpressed␈α
in␈αfirst␈αorder␈α
logic␈αor␈αin␈α
a␈αset
␈↓ ↓H␈↓theory␈αaxiomatized␈α
in␈αfirst␈α
order␈αlogic.␈α
 It␈αhas␈αproved␈α
particularly␈αdifficult␈α
to␈αwork␈α
within␈αlogics
␈↓ ↓H␈↓that␈α∃admit␈α∀only␈α∃continuous␈α∀functions␈α∃and␈α∀predicates.␈α∃ Second,␈α∀proof-checking␈α∃and␈α∀theorem
␈↓ ↓H␈↓proving␈αprograms␈αhave␈αbeen␈αdeveloped␈αfor␈αfirst␈αorder␈αlogic.␈α Finally,␈αfirst␈αorder␈αlogic␈αis␈αcomplete,
␈↓ ↓H␈↓so␈α
that␈αthe␈α
Goedelian␈αincompleteness␈α
of␈αour␈α
theories␈αare␈α
in␈αour␈α
sets␈αof␈α
axioms␈αand␈α
can␈αbe␈α
reduced
␈↓ ↓H␈↓when necessary by additional axioms rather than by having to change the logical system.

␈↓ ↓H␈↓␈↓ α_While␈α↔our␈α↔goal␈α↔is␈α⊗first␈α↔order␈α↔representations␈α↔of␈α⊗recursive␈α↔programs,␈α↔we␈α↔will␈α⊗make
␈↓ ↓H␈↓considerable informal use of higher order functionals and predicates.

␈↓ ↓H␈↓␈↓ α_We␈α⊗present␈α↔two␈α⊗methods␈α↔of␈α⊗representing␈α↔recursive␈α⊗programs.␈α↔ The␈α⊗first␈α↔involves␈α⊗a
␈↓ ↓H␈↓␈↓↓functional␈α⊂equation␈↓␈α⊃and␈α⊂a␈α⊂␈↓↓minimization␈α⊃schema␈↓␈α⊂for␈α⊃each␈α⊂program,␈α⊂and␈α⊃the␈α⊂second␈α⊃defines␈α⊂the
␈↓ ↓H␈↓functions␈α
in␈αterms␈α
of␈αfinite␈α
approximations␈αrepresented␈α
as␈α␈↓↓pair-lists␈↓.␈α
 The␈αfact␈α
that␈αthe␈α
functional
␈↓ ↓H␈↓equation␈α∪of␈α∪a␈α∪program␈α∪can␈α∪be␈α∪simply␈α∪presented␈α∪in␈α∪first␈α∪order␈α∪logic␈α∪was␈α∪first␈α∪presented␈α∪in
␈↓ ↓H␈↓(Cartwright 1977), but the remaining results seem to be new.


␈↓ ↓H␈↓α2. Recursive Programs.

␈↓ ↓H␈↓␈↓ α_An␈α
adequate␈α
background␈α
for␈α
this␈α
paper␈α
is␈α
contained␈α
in␈α
(Manna␈α
1974)␈α
and␈α
more␈α
concisely␈α
in
␈↓ ↓H␈↓(Manna,␈α∂Ness␈α∞and␈α∂Vuillemin␈α∞1973).␈α∂ The␈α∞connections␈α∂of␈α∞recursive␈α∂programs␈α∞with␈α∂second␈α∞order
␈↓ ↓H␈↓logic are given in (Cooper 1969) and (Park 1970).

␈↓ ↓H␈↓␈↓ α_We shall consider mainly ␈↓↓recursive programs␈↓ of the general form

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓f(x) ← ␈↓	t␈↓↓[f](x)␈↓,

␈↓ ↓H␈↓where ␈↓	t␈↓ is a ␈↓↓computable functional␈↓ like

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓␈↓	t␈↓↓ = λf.λx.(␈↓αif␈↓↓ x = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ x . f(x - 1))␈↓,
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 91


␈↓ ↓H␈↓which gives rise to the well known recursive definition of the factorial function, namely

␈↓ ↓H␈↓3)␈↓ α8  ␈↓↓n! = ␈↓αif␈↓↓ n = 0 ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ n . (n - 1)!␈↓.

␈↓ ↓H␈↓␈↓ α_In␈α
general,␈α
we␈α
shall␈α
be␈αinterested␈α
in␈α
partial␈α
functions␈α
from␈αa␈α
domain␈α
D1␈α
to␈α
a␈α
domain␈αD2,
␈↓ ↓H␈↓and␈α
it␈α
will␈α
often␈αbe␈α
necessary␈α
to␈α
augment␈αthese␈α
domains␈α
by␈α
an␈αundefined␈α
element␈α
denoted␈α
by␈α␈↓	w␈↓
␈↓ ↓H␈↓giving␈αrise␈αto␈αdomains␈αD1␈↓∧+␈↓␈αand␈αD2␈↓∧+␈↓.␈α A␈αset␈α␈↓↓F␈↓␈αof␈αtotal␈αbase␈αfunctions␈αon␈αthe␈αdomains␈α
is␈αassumed
␈↓ ↓H␈↓available, and we study functions ␈↓↓computable in the set F␈↓.

␈↓ ↓H␈↓␈↓ α_It␈αis␈αimportant␈αto␈αdistinguish␈αbetween␈αa␈αprogram␈αas␈αa␈αtext␈αand␈αthe␈αpartial␈αfunction␈αdefined
␈↓ ↓H␈↓by␈α⊃the␈α⊃program␈α⊂when␈α⊃one␈α⊃is␈α⊂interested␈α⊃in␈α⊃describing␈α⊂the␈α⊃dependence␈α⊃of␈α⊂the␈α⊃function␈α⊃on␈α⊂the
␈↓ ↓H␈↓interpretation␈α
of␈α
the␈α
basic␈αfunction␈α
and␈α
predicate␈α
symbols.␈α
 However,␈αwe␈α
will␈α
be␈α
working␈αwith␈α
just
␈↓ ↓H␈↓one␈α
interpretation␈α
at␈αa␈α
time,␈α
so␈αwe␈α
won't␈α
use␈αseparate␈α
symbols␈α
for␈αprograms␈α
and␈α
the␈αfunctions␈α
they
␈↓ ↓H␈↓define.


␈↓ ↓H␈↓α3. The Functional Equation of a Recursive Program.

␈↓ ↓H␈↓␈↓ α_Consider the Lisp program

␈↓ ↓H␈↓4)␈↓ α8  ␈↓↓subst(x,y,z) ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ z ␈↓αthen␈↓↓ (␈↓αif␈↓↓ z=y ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ z) ␈↓αelse␈↓↓ subst(x,y,␈↓αa␈↓↓ z) . subst(x,y,␈↓αd␈↓↓ z)␈↓,

␈↓ ↓H␈↓which is also written

␈↓ ↓H␈↓␈↓ α_(DE␈αSUBST␈α(X␈αY␈αZ)␈α(COND␈α((ATOM␈αZ)␈α(COND␈α((EQUAL␈αZ␈αY)␈αX)␈α(T␈αZ)))␈α(T␈α(CONS
␈↓ ↓H␈↓(SUBST X Y (CAR Z)) (SUBST X Y (CDR Z)))))).

␈↓ ↓H␈↓␈↓ α_The␈α∞basic␈α
functions␈α∞{␈↓↓car,␈α
cdr,␈α∞cons,␈α
atom}␈↓␈α∞of␈α∞Lisp␈α
are␈α∞all␈α
assumed␈α∞total,␈α
but␈α∞we␈α∞will␈α
say
␈↓ ↓H␈↓nothing␈α∞about␈α∞the␈α∞values␈α∞of␈α∞␈↓↓car␈↓␈α∞and␈α∞␈↓↓cdr␈↓␈α∞when␈α∞applied␈α∞to␈α∞atoms.␈α∞ According␈α∞to␈α∞the␈α∞fixed␈α∞point
␈↓ ↓H␈↓theory␈α
of␈α
recursive␈α
programs,␈α
this␈α
program␈α
defines␈α
a␈α
function␈α
from␈α
␈↓↓Sexp␈↓␈α
(the␈α
set␈αof␈α
S-expressions)
␈↓ ↓H␈↓to␈αSexp␈↓∧+␈↓␈α(the␈αset␈αof␈αS-expressions␈αaugmented␈αby␈α␈↓	w␈↓).␈α This␈αfunction␈αcan␈αbe␈αcomputed␈αby␈αany␈α␈↓↓safe
␈↓ ↓H␈↓↓computation␈αrule␈↓,␈αand␈αwhen␈αthe␈αcomputation␈αterminates,␈αits␈αvalue␈αwill␈αbelong␈αto␈α␈↓↓Sexp.␈↓␈α When␈αthe
␈↓ ↓H␈↓computation␈α⊃doesn't␈α⊃terminate,␈α∩the␈α⊃value␈α⊃of␈α∩␈↓↓f(x)␈↓␈α⊃is␈α⊃␈↓	w␈↓.␈α∩ While␈α⊃this␈α⊃particular␈α∩function␈α⊃always
␈↓ ↓H␈↓terminates,␈α
we␈α
do␈α
not␈α
assume␈α∞it␈α
in␈α
writing␈α
our␈α
first␈α
order␈α∞formula.␈α
 Indeed␈α
we␈α
will␈α
use␈α∞the␈α
first
␈↓ ↓H␈↓order formula to prove termination by structural induction.

␈↓ ↓H␈↓␈↓ α_These facts show that the function ␈↓↓subst␈↓ defined recursively by (4) satisfies the sentence

␈↓ ↓H␈↓5)␈↓ α8␈α⊃ ␈↓↓∀x␈α⊃y␈α⊃z.(subst(x,y,z)␈α⊃=␈α⊂␈↓αif␈↓↓␈α⊃␈↓αat␈↓↓␈α⊃z␈α⊃␈↓αthen␈↓↓␈α⊃(␈↓αif␈↓↓␈α⊂z␈α⊃=␈α⊃y␈α⊃␈↓αthen␈↓↓␈α⊃x␈α⊂␈↓αelse␈↓↓␈α⊃z)␈α⊃␈↓αelse␈↓↓␈α⊃subst(x,y,␈↓αa␈↓↓␈α⊃z)␈α⊂.
␈↓ ↓H␈↓↓subst(x,y,␈↓αd␈↓↓ z))␈↓

␈↓ ↓H␈↓of␈α
first␈αorder␈α
logic.␈α
 The␈αvariables␈α
␈↓↓x,␈αy␈↓␈α
and␈α
␈↓↓z␈↓␈αrange␈α
over␈α␈↓↓Sexp;␈↓␈α
when␈α
we␈αwant␈α
to␈α
quantify␈αover
␈↓ ↓H␈↓␈↓↓Sexp␈↓∧+␈↓,␈α
we␈α
use␈α␈↓↓X,␈α
Y␈α
␈↓and␈↓↓␈α
Z␈↓.␈α Moreover,␈α
we␈α
are␈α
augmenting␈αfirst␈α
order␈α
logic␈α
by␈αallowing␈α
conditional
␈↓ ↓H␈↓expressions␈αas␈αterms.␈α The␈αaugmentation␈αis␈αinessential,␈αbecause␈αconditional␈αexpressions␈αcan␈αalways
␈↓ ↓H␈↓be eliminated from sentences by distributing predicates over them.  Thus (5) can be written

␈↓ ↓H␈↓6)␈↓ α8␈α ␈↓↓∀x␈αy␈αz.(␈↓αat␈↓↓␈αz␈α⊃␈α(z=y␈α⊃␈αsubst(x,y,z)␈α=␈α
x)␈α∧␈αz≠y␈α⊃␈αsubst(x,y,z)␈α=␈αz)␈α∧␈α¬␈↓αat␈↓↓␈αz␈α⊃␈α
subst(x,y,z)
␈↓ ↓H␈↓↓= subst(x,y,␈↓αa␈↓↓ z) . subst(x,y,␈↓αd␈↓↓ z)),␈↓

␈↓ ↓H␈↓but the conditional expression is clearer and closer to the program.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 92


␈↓ ↓H␈↓␈↓ α_A␈αgoal␈α
of␈αour␈α
first␈αorder␈α
representation␈αwould␈αbe␈α
to␈αuse␈α
(4)␈αonly␈α
to␈αjustify␈α
writing␈α(5)␈α(or␈α
(6)
␈↓ ↓H␈↓if␈αyou␈αdon't␈αlike␈αconditional␈αexpressions␈αin␈αthe␈αlogic)␈αand␈αthen␈αprove␈αall␈αproperties␈αof␈α␈↓↓subst␈↓␈αusing
␈↓ ↓H␈↓a first order axiomatization of Lisp.




␈↓ ↓H␈↓α4. First Order Axioms for Lisp.

␈↓ ↓H␈↓␈↓ α_We␈α⊂use␈α⊃lower␈α⊂case␈α⊂variables␈α⊃␈↓↓x,␈↓␈α⊂␈↓↓y,␈↓␈α⊃and␈α⊂␈↓↓z␈↓␈α⊂with␈α⊃or␈α⊂without␈α⊂subscripts␈α⊃to␈α⊂range␈α⊃over␈α⊂S-
␈↓ ↓H␈↓expressions.␈α Capitalized␈αvariables␈αrange␈αover␈αall␈αentities.␈α
 We␈αalso␈αuse␈αvariables␈α␈↓↓u,␈↓␈α␈↓↓v␈↓␈αand␈α␈↓↓w␈↓␈α
with
␈↓ ↓H␈↓or␈α∂without␈α∂subscripts␈α∂to␈α∂range␈α∂over␈α∂lists,␈α∂i.e.␈α∂S-expressions␈α∂such␈α∂that␈α∂successive␈α∂␈↓↓cdr␈↓s␈α∂eventually
␈↓ ↓H␈↓reach␈αNIL.␈α (The␈α␈↓↓car␈↓␈αof␈αa␈αlist␈αis␈αnot␈αrequired␈αto␈αbe␈αa␈αlist).␈α We␈αuse␈αpredicates␈α␈↓↓issexp␈↓␈αand␈α␈↓↓islist␈↓␈αto
␈↓ ↓H␈↓assert␈α∪that␈α∪an␈α∀individual␈α∪is␈α∪an␈α∀S-expression␈α∪or␈α∪a␈α∪list.␈α∀ First␈α∪come␈α∪the␈α∀"housekeeping"␈α∪and
␈↓ ↓H␈↓"algebraic" axioms:

␈↓ ↓H␈↓L1:     ␈↓↓∀x.issexp x␈↓

␈↓ ↓H␈↓L2:     ␈↓↓∀u.islist u␈↓

␈↓ ↓H␈↓L3:     ␈↓↓∀u.issexp u␈↓

␈↓ ↓H␈↓L4:     ␈↓↓¬issexp ␈↓	w␈↓

␈↓ ↓H␈↓L5:     ␈↓↓islist ␈↓NIL

␈↓ ↓H␈↓L6:     ␈↓↓␈↓αat␈↓↓ ␈↓NIL␈↓↓␈↓

␈↓ ↓H␈↓L7:     ␈↓↓∀u.(␈↓αat␈↓↓ u ⊃ u = ␈↓NIL␈↓↓)␈↓

␈↓ ↓H␈↓L8:     ␈↓↓∀x y.issexp (x.y)␈↓

␈↓ ↓H␈↓L9:     ␈↓↓∀x u.islist (x.u)␈↓

␈↓ ↓H␈↓L10:    ␈↓↓∀x. ¬␈↓αat␈↓↓ x ⊃ issexp ␈↓αa␈↓↓ x␈↓

␈↓ ↓H␈↓L11:    ␈↓↓∀x. ¬␈↓αat␈↓↓ x ⊃ issexp ␈↓αd␈↓↓ x␈↓

␈↓ ↓H␈↓L12:    ␈↓↓∀u. u ≠ ␈↓NIL␈↓↓ ⊃ islist ␈↓αd␈↓↓ u␈↓

␈↓ ↓H␈↓L13:    ␈↓↓∀x y. ␈↓αa␈↓↓ (x.y) = x␈↓

␈↓ ↓H␈↓L14:    ␈↓↓∀x y. ␈↓αd␈↓↓ (x.y) = y␈↓

␈↓ ↓H␈↓L15:    ␈↓↓∀x y. ¬␈↓αat␈↓↓ (x.y)␈↓

␈↓ ↓H␈↓L16:    ␈↓↓∀x.¬␈↓αat␈↓↓ x ⊃ (␈↓αa␈↓↓ x . ␈↓αd␈↓↓ x) = x␈↓

␈↓ ↓H␈↓␈↓ α_Next we have axiom schemata of induction
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 93


␈↓ ↓H␈↓LS1:    ␈↓↓(∀x.␈↓αat␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ∧ ∀x.(¬␈↓αat␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αa␈↓↓ x ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ x ⊃ ␈↓	F␈↓↓ x) ⊃ ∀x.␈↓	F␈↓↓ x␈↓

␈↓ ↓H␈↓LS2:    ␈↓↓(∀u.u = ␈↓NIL␈↓↓ ⊃ ␈↓	F␈↓↓ u) ∧ ∀u.(u ≠ ␈↓NIL␈↓↓ ∧ ␈↓	F␈↓↓ ␈↓αd␈↓↓ u ⊃ ␈↓	F␈↓↓ u) ⊃ ∀u. ␈↓	F␈↓↓ u␈↓.

␈↓ ↓H␈↓␈↓ α_From these axioms and schemata, we can prove

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓∀x y z.issexp subst(x,y,z)␈↓

␈↓ ↓H␈↓which␈α
is␈α
our␈α
way␈α
of␈α
saying␈αthat␈α
␈↓↓subst␈↓␈α
is␈α
total.␈α
 The␈α
key␈αstep␈α
is␈α
applying␈α
the␈α
axiom␈α
schema␈αLS1
␈↓ ↓H␈↓with␈α∂the␈α∂predicate␈α∞␈↓↓␈↓	F␈↓↓(z)␈α∂≡␈α∂issexp(x,y,z)␈↓.␈α∂ We␈α∞can␈α∂also␈α∂prove␈α∂in␈α∞first␈α∂order␈α∂logic␈α∂such␈α∞algebraic
␈↓ ↓H␈↓properties of ␈↓↓subst␈↓ as

␈↓ ↓H␈↓8)␈↓ α8  ␈↓↓∀x y z y1 z1.(¬occur(y,z1) ⊃ subst(subst(x,y,z),y1,z1) = subst(x,y,subst(z,y1,z1)))␈↓

␈↓ ↓H␈↓if␈αwe␈αhave␈αsuitable␈αaxiomatization␈αof␈αthe␈αpredicate␈α␈↓↓occur(x,y)␈↓␈αmeaning␈αthat␈αthe␈αatom␈α␈↓↓x␈↓␈αoccurs␈αin
␈↓ ↓H␈↓the S-expression ␈↓↓y.␈↓

␈↓ ↓H␈↓␈↓ α_The␈α
axiomatization␈α
of␈α
the␈α
predicate␈α
␈↓↓occur␈↓␈α
raises␈α
some␈α
new␈α
problems.␈α
 It␈α
is␈α
defined␈α∞by␈α
the
␈↓ ↓H␈↓recursive Lisp program

␈↓ ↓H␈↓9)␈↓ α8  ␈↓↓occur(x,y) ← (x = y) ∨ (¬␈↓αat␈↓↓ y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y)))␈↓.

␈↓ ↓H␈↓If␈α∂we␈α∂were␈α∂sure␈α∂in␈α∞advance␈α∂that␈α∂␈↓↓occur␈↓␈α∂were␈α∂total,␈α∂we␈α∞could␈α∂translate␈α∂the␈α∂recursion␈α∂(9)␈α∂into␈α∞the
␈↓ ↓H␈↓sentence

␈↓ ↓H␈↓10)␈↓ α8  ␈↓↓∀x y.(occur(x,y) ≡ (x = y) ∨ (¬␈↓αat␈↓↓ y ∧ (occur(x,␈↓αa␈↓↓ y) ∨ occur(x,␈↓αd␈↓↓ y))))␈↓

␈↓ ↓H␈↓which␈α⊂will␈α∂suffice␈α⊂for␈α∂proving␈α⊂(8),␈α∂but␈α⊂we␈α∂have␈α⊂no␈α∂right␈α⊂to␈α∂write␈α⊂it␈α∂down␈α⊂from␈α⊂the␈α∂recursive
␈↓ ↓H␈↓definition (9).

␈↓ ↓H␈↓␈↓ α_What we can write is the definition

␈↓ ↓H␈↓11)␈↓ α8  ␈↓↓∀x y.(occura(x,y) = (x equals y) or (not atom y and (occura(x,␈↓αa␈↓↓ y) or occura(x,␈↓αd␈↓↓ y))))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓12)␈↓ α8  ␈↓↓∀x y.(occur(x,y) ≡ (occura(x,y) = T))␈↓

␈↓ ↓H␈↓from which (10) can eventually be proved in first order logic.

␈↓ ↓H␈↓␈↓ α_Since␈αrecursive␈αdefinitions␈αgive␈αrise␈αto␈αpartial␈α
predicates,␈αand␈αwe␈αdon't␈αwant␈αto␈αuse␈αa␈α
partial
␈↓ ↓H␈↓predicate␈α∞logic,␈α∞we␈α∞introduce␈α∂a␈α∞domain␈α∞␈↓	P␈↓␈α∞of␈α∂␈↓↓extended␈α∞truth␈α∞values␈↓␈α∞with␈α∂characteristic␈α∞predicate
␈↓ ↓H␈↓␈↓↓isetv␈↓ whose elements are ␈↓↓T,␈↓ ␈↓↓F␈↓ and ␈↓	w␈↓.  The following axioms describe functions into or out of ␈↓	P␈↓↓.

␈↓ ↓H␈↓B1:     ␈↓↓∀p.(isetv p)␈↓

␈↓ ↓H␈↓B2:     ␈↓↓∀p.(p = T ∨ p = F ∨ p = ␈↓	w␈↓↓)␈↓

␈↓ ↓H␈↓B3:     ␈↓↓T ≠ F ∧ T ≠ ␈↓	w␈↓↓ ∧ F ≠ ␈↓	w␈↓
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 94


␈↓ ↓H␈↓B4:     ␈↓↓∀p. isetv not p␈↓

␈↓ ↓H␈↓B5:     ␈↓↓∀p q. isetv(p and q)␈↓

␈↓ ↓H␈↓B6:     ␈↓↓∀p q. isetv(p or q)␈↓

␈↓ ↓H␈↓B7:     ␈↓↓∀p.(not p = ␈↓αif␈↓↓ (p = ␈↓	w␈↓↓) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ F ␈↓αelse␈↓↓ T)␈↓

␈↓ ↓H␈↓B8:     ␈↓↓∀p q.(p and q = ␈↓αif␈↓↓ (p = ␈↓	w␈↓↓) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ q ␈↓αelse␈↓↓ F)␈↓

␈↓ ↓H␈↓B9:     ␈↓↓∀p q.(p or q = (␈↓αif␈↓↓ p = ␈↓	w␈↓↓) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ q)␈↓

␈↓ ↓H␈↓B10:    ␈↓↓∀X Y.(X equal Y = ␈↓αif␈↓↓ ¬issexp X ∨ ¬issexp Y ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ X = Y ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓

␈↓ ↓H␈↓B11:    ␈↓↓∀X.(aatom X = ␈↓αif␈↓↓ ¬issexp X ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αat␈↓↓ X ␈↓αthen␈↓↓ T ␈↓αelse␈↓↓ F)␈↓,

␈↓ ↓H␈↓and we also need a conditional expression that can take an argument from ␈↓	P␈↓, namely

␈↓ ↓H␈↓B12:    ␈↓↓∀p X Y.(if(p,X,Y) = ␈↓αif␈↓↓ p = ␈↓	w␈↓↓ ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ p = T ␈↓αthen␈↓↓ X ␈↓αelse␈↓↓ Y)␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓occura␈↓␈α
is␈α
proved␈α
total␈α
by␈α
applying␈α
schema␈αLS1␈α
with␈α
␈↓↓␈↓	F␈↓↓(y)␈α
≡␈α
occura(x,y)␈α
≠␈α
␈↓	w␈↓↓␈↓.␈α
 After␈αthis␈α
␈↓↓occur␈↓
␈↓ ↓H␈↓can be shown to satisfy (10).

␈↓ ↓H␈↓␈↓ α_The␈α∂axioms␈α∂L1-L16␈α∂and␈α∂B1-B12␈α∂together␈α∂with␈α∂the␈α∂sentences␈α∂arising␈α∂from␈α∂the␈α∂schemata
␈↓ ↓H␈↓LS1␈αand␈αLS2␈αwill␈αbe␈αcalled␈αthe␈αaxiom␈αsystem␈αLisp0.␈α We␈αwill␈αadjoin␈αone␈αmore␈αaxiom␈αlater␈αto␈αget
␈↓ ↓H␈↓the system Lisp1.

␈↓ ↓H␈↓␈↓ α_The␈αabove␈α
method␈αof␈α
replacing␈αa␈α
recursion␈αby␈αa␈α
first␈αorder␈α
sentence␈αwas␈α
first␈α(I␈αthink)␈α
used
␈↓ ↓H␈↓in (Cartwright 1977).  It seems surprising that it wasn't invented sooner.



␈↓ ↓H␈↓α5. The Minimization Schema.

␈↓ ↓H␈↓␈↓ α_The␈αfunctional␈αequation␈α
of␈αa␈αprogram␈αdoesn't␈α
completely␈αcharacterize␈αit.␈α For␈α
example,␈αthe
␈↓ ↓H␈↓program

␈↓ ↓H␈↓13)␈↓ α8 ␈↓↓f1 x ← f1 x␈↓

␈↓ ↓H␈↓leads to the sentence

␈↓ ↓H␈↓14)␈↓ α8 ␈↓↓∀x.(f1 x = f1 x)␈↓

␈↓ ↓H␈↓which␈αprovides␈α
no␈αinformation␈α
although␈αthe␈α
function␈α␈↓↓f␈↓␈α
is␈αundefined␈α
for␈αall␈α
␈↓↓x.␈↓␈α This␈α
is␈αnot␈α
always
␈↓ ↓H␈↓the case, since the program

␈↓ ↓H␈↓15)␈↓ α8 ␈↓↓f2 x ← (f2 x).␈↓NIL␈↓↓␈↓

␈↓ ↓H␈↓has the functional equation
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 95


␈↓ ↓H␈↓16)␈↓ α8 ␈↓↓∀x.(f2 x = (f2 x).␈↓NIL␈↓↓)␈↓.

␈↓ ↓H␈↓from which ␈↓↓∀x.¬issexp f2(x)␈↓ can be proved by induction.

␈↓ ↓H␈↓␈↓ α_In␈α⊃order␈α⊂to␈α⊃characterize␈α⊃recursive␈α⊂programs,␈α⊃we␈α⊃need␈α⊂some␈α⊃way␈α⊃of␈α⊂asking␈α⊃for␈α⊃the␈α⊂least
␈↓ ↓H␈↓defined solution of the functional equation.

␈↓ ↓H␈↓␈↓ α_Suppose the program is

␈↓ ↓H␈↓17)␈↓ α8 ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓

␈↓ ↓H␈↓yielding the functional equation

␈↓ ↓H␈↓18)␈↓ α8 ␈↓↓∀x.(f x = ␈↓	t␈↓↓[f](x)␈↓.

␈↓ ↓H␈↓The ␈↓↓minimization schema␈↓ is then

␈↓ ↓H␈↓19)␈↓ α8 ␈↓↓∀x.(isD ␈↓	t␈↓↓[␈↓	f␈↓↓](x) ⊃ ␈↓	f␈↓↓ x = ␈↓	t␈↓↓[␈↓	f␈↓↓](x)) ⊃ ∀x.(isD f x ⊃ ␈↓	f␈↓↓ x = f x)␈↓.

␈↓ ↓H␈↓␈↓ α_In the ␈↓↓subst␈↓ example, the schema is

␈↓ ↓H␈↓20)␈↓ α8␈α⊂␈↓↓∀x␈α⊂y␈α⊂z.(issexp␈α⊂(␈↓αif␈↓↓␈α⊂␈↓αat␈↓↓␈α∂z␈α⊂␈↓αthen␈↓↓␈α⊂(␈↓αif␈↓↓␈α⊂z␈α⊂=␈α⊂y␈α⊂␈↓αthen␈↓↓␈α∂x␈α⊂␈↓αelse␈↓↓␈α⊂z)␈α⊂␈↓αelse␈↓↓␈α⊂␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α⊂z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α⊂z))␈α∂⊃
␈↓ ↓H␈↓↓␈↓	f␈↓↓(x,y,z)␈α∂=␈α∂␈↓αif␈↓↓␈α∞␈↓αat␈↓↓␈α∂z␈α∂␈↓αthen␈↓↓␈α∞(␈↓αif␈↓↓␈α∂z␈α∂=␈α∞y␈α∂␈↓αthen␈↓↓␈α∂x␈α∞␈↓αelse␈↓↓␈α∂z)␈α∂␈↓αelse␈↓↓␈α∞␈↓	f␈↓↓(x,y,␈↓αa␈↓↓␈α∂z).␈↓	f␈↓↓(x,y,␈↓αd␈↓↓␈α∂z))␈α∞⊃␈α∂∀x␈α∂y␈α∞z.(issexp
␈↓ ↓H␈↓↓subst(x,y,z) ⊃ ␈↓	f␈↓↓(x,y,z) = subst(x,y,z))␈↓.

␈↓ ↓H␈↓␈↓ α_In␈αthe␈αschema␈α␈↓	f␈↓␈αis␈αa␈αfree␈αfunction␈αvariable␈αof␈αthe␈αappropriate␈αnumber␈αof␈αarguments.␈α The
␈↓ ↓H␈↓schema is just a translation into first order logic of Park's (1970) theorem

␈↓ ↓H␈↓21)␈↓ α8 ␈↓↓␈↓	f␈↓↓ ␈↓πd␈↓↓ ␈↓	t␈↓↓[␈↓	f␈↓↓] ⊃ ␈↓	f␈↓↓ ␈↓πd␈↓↓ Y[␈↓	t␈↓↓]␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α
simplest␈α
application␈α
of␈αthe␈α
schema␈α
is␈α
to␈αshow␈α
that␈α
the␈α
␈↓↓f1␈↓␈α
defined␈αby␈α
(13)␈α
is␈α
never␈αan␈α
S-
␈↓ ↓H␈↓expression.  The schema becomes

␈↓ ↓H␈↓22)␈↓ α8 ␈↓↓∀x.(issexp ␈↓	f␈↓↓ x ⊃ ␈↓	f␈↓↓ x = ␈↓	f␈↓↓ x) ⊃ ∀x.(issexp f1 x ⊃ ␈↓	f␈↓↓ x = f1 x)␈↓,

␈↓ ↓H␈↓and we take

␈↓ ↓H␈↓23)␈↓ α8 ␈↓↓␈↓	f␈↓↓ x = ␈↓	w␈↓↓␈↓.

␈↓ ↓H␈↓The␈αleft␈αside␈αof␈α(22)␈αis␈αidentically␈αtrue,␈αand,␈αremembering␈αthat␈α␈↓	w␈↓␈αis␈αnot␈αan␈αS-expression,␈αthe␈αright
␈↓ ↓H␈↓side tells us that ␈↓↓f1 x␈↓ is never an S-expression.

␈↓ ↓H␈↓␈↓ α_The␈αminimization␈αschema␈αcan␈αsometimes␈αbe␈αused␈αto␈αshow␈αpartial␈αcorrectness.␈α For␈αexample,
␈↓ ↓H␈↓the well known 91-function is defined by the recursive program over the integers

␈↓ ↓H␈↓24)␈↓ α8 ␈↓↓f91 x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ f91 f91(x + 11)␈↓.

␈↓ ↓H␈↓The goal is to show that

␈↓ ↓H␈↓25)␈↓ α8 ␈↓↓∀x.(f91 x = ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ 91 ␈↓αelse␈↓↓ 91␈↓.
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 96


␈↓ ↓H␈↓We apply the minimization schema with

␈↓ ↓H␈↓26)␈↓ α8 ␈↓↓␈↓	f␈↓↓ x ← ␈↓αif␈↓↓ x > 100 ␈↓αthen␈↓↓ x - 10 ␈↓αelse␈↓↓ 91␈↓,

␈↓ ↓H␈↓and␈α
it␈αcan␈α
be␈α
shown␈αby␈α
an␈α
explicit␈αcalculation␈α
without␈α
induction␈αthat␈α
the␈α
premiss␈αof␈α
the␈αschema␈α
is
␈↓ ↓H␈↓satisfied, and this shows that ␈↓↓f91,␈↓ whenever defined has the desired value.

␈↓ ↓H␈↓␈↓ α_The␈α
method␈α
of␈α
recursion␈α
induction␈α
(McCarthy␈α1963)␈α
is␈α
also␈α
an␈α
immediate␈α
application␈αof␈α
the
␈↓ ↓H␈↓minimization␈α
schema.␈α
 If␈α
we␈α
show␈α
that␈α
two␈αfunctions␈α
satisfy␈α
the␈α
schema␈α
of␈α
a␈α
recursive␈αprogram,
␈↓ ↓H␈↓we␈α
show␈α
that␈αthey␈α
both␈α
equal␈α
the␈αfunction␈α
computed␈α
by␈α
the␈αprogram␈α
on␈α
whereever␈α
the␈αfunction␈α
is
␈↓ ↓H␈↓defined.

␈↓ ↓H␈↓␈↓ α_The␈α
utility␈α
of␈α
the␈α
minimization␈αschema␈α
for␈α
proving␈α
partial␈α
correctness␈α
or␈αnon-termination
␈↓ ↓H␈↓depends␈α∂on␈α∂our␈α∞ability␈α∂to␈α∂name␈α∂suitable␈α∞comparison␈α∂functions.␈α∂ f1␈α∞and␈α∂f91␈α∂were␈α∂easily␈α∞treated,
␈↓ ↓H␈↓because␈α⊃the␈α⊃necessary␈α⊃comparison␈α⊃functions␈α⊃could␈α⊃be␈α⊃given␈α⊃explicitly␈α⊃without␈α⊃recursion.␈α⊂ Any
␈↓ ↓H␈↓extension␈αof␈αthe␈αlanguage␈αthat␈αprovides␈αnew␈αtools␈αfor␈αnaming␈αcomparison␈αfunctions,␈αe.g.␈αgoing␈αto
␈↓ ↓H␈↓higher order logic, will improve our ability to use the schema in proofs.

␈↓ ↓H␈↓␈↓ α_(19)␈α∂can␈α∞be␈α∂regarded␈α∞as␈α∂an␈α∞axiom␈α∂schema␈α∞involving␈α∂a␈α∞second␈α∂order␈α∞function␈α∂variable␈α∞␈↓	t␈↓.
␈↓ ↓H␈↓What␈αcan␈α
be␈αsubstituted␈α
for␈α␈↓	t␈↓␈α
is␈αa␈α quantifier␈α
free␈αλ-expression␈α
in␈αa␈α
first␈αorder␈αfunction␈α
variable.
␈↓ ↓H␈↓It␈α
may␈α
be␈α
interesting␈α
to␈α
study␈α
the␈α
sets␈α
of␈α
first␈α
order␈α
sentences␈α
that␈α
can␈α
be␈α
generated␈α
by␈αsuch␈α
second
␈↓ ↓H␈↓order␈αsentence␈αschemata.␈α Presumably,␈αsets␈αof␈αsentences␈αcan␈αbe␈αgenerated␈αin␈αthis␈αway␈αthat␈αcannnot
␈↓ ↓H␈↓be generated by schemata with only first order function variables.



␈↓ ↓H␈↓α6. Proof Methods as Axiom Schemata

␈↓ ↓H␈↓␈↓ α_Representing␈α
recursive␈α
definitions␈α
in␈αfirst␈α
order␈α
logic␈α
permits␈αus␈α
to␈α
express␈α
some␈αwell␈α
known
␈↓ ↓H␈↓methods for proving partial correctness as axiom schemata of first order logic.

␈↓ ↓H␈↓␈↓ α_For example, suppose we want to prove that if the input ␈↓↓x␈↓ of a function ␈↓↓f␈↓ defined by

␈↓ ↓H␈↓27)␈↓ α8  ␈↓↓f x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ f h x␈↓

␈↓ ↓H␈↓satisfies␈α
␈↓↓␈↓	F␈↓↓(x)␈↓,␈αthen␈α
if␈α
the␈αfunction␈α
terminates,␈αthe␈α
output␈α
␈↓↓f(x)␈↓␈αwill␈α
satisfy␈α
␈↓	Y␈↓↓(f(x))␈↓.␈α We␈α
appeal␈αto␈α
the
␈↓ ↓H␈↓following ␈↓↓axiom schema of inductive assertions␈↓:

␈↓ ↓H␈↓28)␈↓ α8  ␈↓↓∀x.(␈↓	F␈↓↓(x) ⊃ q(x,x)) ∧ ∀x y.(q(x,y) ⊃ ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ ␈↓	Y␈↓↓(x,y) ␈↓αelse␈↓↓ q(x,␈↓π ␈↓↓h y))
␈↓ ↓H␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ inrange f x ⊃ ␈↓	Y␈↓↓(x,f x))␈↓


␈↓ ↓H␈↓where␈α␈↓↓inrange␈αf␈αx␈↓␈αis␈αthe␈αassertion␈αthat␈α␈↓↓f(x)␈↓␈αis␈αin␈αthe␈αnominal␈αrange␈αof␈αthe␈αfunction␈αdefinition,␈αi.e.
␈↓ ↓H␈↓is␈αan␈αinteger␈αor␈αan␈αS-expression␈αas␈αthe␈αcase␈αmay␈αbe,␈αand␈αasserts␈αthat␈αthe␈αcomputation␈αterminates.
␈↓ ↓H␈↓In␈α
order␈α
to␈α
use␈α
the␈α∞schema,␈α
we␈α
must␈α
invent␈α
a␈α
suitable␈α∞predicate␈α
␈↓↓q(x,y)␈↓,␈α
and␈α
this␈α
is␈α∞precisely␈α
the
␈↓ ↓H␈↓method␈αof␈αinductive␈αassertions.␈α The␈αschema␈αis␈αvalid␈αfor␈αall␈αpredicates␈α␈↓	F␈↓,␈α␈↓	Y␈↓,␈αand␈α␈↓↓q␈↓,␈αand␈αa␈αsimilar
␈↓ ↓H␈↓schema can be written for any collection of mutually recursive definitions that is iterative.

␈↓ ↓H␈↓␈↓ α_The␈α⊂method␈α⊂of␈α⊂␈↓↓subgoal␈α∂induction␈↓,␈α⊂(Manna␈α⊂and␈α⊂Pnueli␈α∂1970)␈α⊂and␈α⊂(Morris␈α⊂and␈α∂Wegbreit
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 97


␈↓ ↓H␈↓1977),␈α∩is␈α∪not␈α∩limited␈α∪to␈α∩iterative␈α∪definitions.␈α∩ Thus␈α∩it␈α∪can␈α∩be␈α∪formulated␈α∩for␈α∪such␈α∩recursive
␈↓ ↓H␈↓programs as

␈↓ ↓H␈↓29)␈↓ α8  ␈↓↓f␈↓β5␈↓↓ x ← ␈↓αif␈↓↓ p x ␈↓αthen␈↓↓ h x ␈↓αelse␈↓↓ g1 f␈↓β5␈↓↓ g2 x␈↓,

␈↓ ↓H␈↓where ␈↓↓p␈↓ must be assumed total.  The schema is

␈↓ ↓H␈↓30)␈↓ α8  ␈↓↓∀x.(p x ⊃ q(x,h x)) ∧ ∀x z.(¬p(x) ∧ q(g2 x,z) ⊃ q(x,g1 z)) ∧ ∀x.(␈↓	F␈↓↓(x) ∧ q(x,z) ⊃ ␈↓	Y␈↓↓(x,z))
␈↓ ↓H␈↓↓                ⊃ ∀x.(␈↓	F␈↓↓(x) ∧ inrange(f(x)) ⊃ ␈↓	Y␈↓↓(x,f(x)))␈↓

␈↓ ↓H␈↓␈↓ α_The␈α∩possibility␈α∩of␈α∩expressing␈α∩these␈α∩methods␈α∩as␈α∩axiom␈α∩schemata␈α∩depends␈α∩on␈α∩using␈α∩the
␈↓ ↓H␈↓predicate␈α⊃␈↓↓inrange␈↓␈α∩to␈α⊃express␈α⊃termination.␈α∩ The␈α⊃minimization␈α⊃schema␈α∩itself␈α⊃can␈α⊃be␈α∩proved␈α⊃by
␈↓ ↓H␈↓subgoal induction.  We need only take ␈↓↓␈↓	F␈↓↓(x) ≡ ␈↓αtrue␈↓ and ␈↓	Y␈↓↓(x,y) ≡ q(x,y) = (y = ␈↓	f␈↓↓(x)␈↓.

␈↓ ↓H␈↓␈↓ α_We␈α
have␈αnot␈α
given␈α
a␈αgeneral␈α
rule␈α
for␈αgoing␈α
from␈α
the␈αrecursive␈α
definition␈α
(or␈αequivalently
␈↓ ↓H␈↓from␈α∞the␈α
functional␈α∞equation␈α
and␈α∞minimization␈α
schema)␈α∞to␈α
the␈α∞schema␈α
of␈α∞subgoal␈α∞induction.␈α
 It
␈↓ ↓H␈↓doesn't␈α∂seem␈α∂to␈α∞be␈α∂a␈α∂schema␈α∞in␈α∂␈↓	t␈↓.␈α∂ Such␈α∞a␈α∂rule␈α∂can␈α∞be␈α∂adapted␈α∂from␈α∞the␈α∂one␈α∂in␈α∂(Manna␈α∞and
␈↓ ↓H␈↓Pnueli␈α∩1970)␈α∩using␈α∩the␈α∩␈↓↓inrange␈↓␈α∩predicate␈α∩in␈α∩the␈α∩construction␈α∩of␈α∩the␈α∩right␈α∩hand␈α∩side␈α∩of␈α∩the
␈↓ ↓H␈↓implication.




␈↓ ↓H␈↓α7. Representations Using Finite Approximations.

␈↓ ↓H␈↓␈↓ α_Our␈αsecond␈αapproach␈αto␈αrepresenting␈αrecursive␈αprograms␈αby␈αfirst␈αorder␈αformulas␈αgoes␈αback
␈↓ ↓H␈↓to␈α∂Goedel␈α∂(1931,␈α∞1934)␈α∂who␈α∂showed␈α∞that␈α∂primitive␈α∂recursive␈α∞functions␈α∂could␈α∂be␈α∂so␈α∞represented.
␈↓ ↓H␈↓(Our knowledge of Goedel's work comes from (Kleene 1951)).

␈↓ ↓H␈↓␈↓ α_Kleene␈α(1951)␈α
calls␈αa␈αfunction␈α
␈↓↓f␈↓␈α␈↓↓representable␈↓␈αif␈α
there␈αis␈αan␈α
arithmetic␈αformula␈α␈↓↓A␈↓␈α
with␈αfree
␈↓ ↓H␈↓variables ␈↓↓x␈↓ and ␈↓↓y␈↓ such that

␈↓ ↓H␈↓1)␈↓ α8  ␈↓↓∀x y.((y = f(x)) ≡ A)␈↓,

␈↓ ↓H␈↓where␈αan␈αarithmetic␈αformula␈αis␈αbuilt␈αup␈αfrom␈αinteger␈αconstants␈αand␈αvariables␈αusing␈αonly␈αaddition,
␈↓ ↓H␈↓multiplication␈αand␈αbounded␈α
quantification.␈α Kleene␈αshowed␈αthat␈α
all␈αpartial␈αrecursive␈αfunctions␈α
are
␈↓ ↓H␈↓representable.␈α⊗ The␈α⊗proof␈α⊗involves␈α⊗Goedel␈α⊗numbering␈α⊗possible␈α⊗computation␈α↔sequences␈α⊗and
␈↓ ↓H␈↓showing␈αthat␈αthe␈αrelation␈αbetween␈αsequences␈αand␈αtheir␈αelements␈αand␈αthe␈αsteps␈αof␈αthe␈αcomputation
␈↓ ↓H␈↓are all representable.

␈↓ ↓H␈↓␈↓ α_In␈αLisp␈αless␈αmachinery␈α
has␈αto␈αbe␈αbuilt␈α
up,␈αbecause␈αsequences␈αare␈α
Lisp␈αdata,␈αand␈αthe␈α
relation
␈↓ ↓H␈↓between␈α∞a␈α∞sequence␈α∞and␈α∞its␈α∞elements␈α∞is␈α∞given␈α∞by␈α∞basic␈α∞Lisp␈α∞functions␈α∞and␈α∞by␈α∞the␈α∞␈↓↓subexpression
␈↓ ↓H␈↓↓relation␈↓ defined by

␈↓ ↓H␈↓2)␈↓ α8  ␈↓↓x subexp y ← (x = y) ∨ ¬␈↓αat␈↓↓ y ∧ [x subexp ␈↓αa␈↓↓ y ∨ x subexp ␈↓αd␈↓↓ y]␈↓.

␈↓ ↓H␈↓␈↓ α_␈↓↓subexp␈↓␈α
is␈α
the␈α
only␈α
recursive␈α
definition␈α
we␈α∞shall␈α
require.␈α
 Since␈α
it␈α
is␈α
total,␈α
we␈α
only␈α∞need␈α
its
␈↓ ↓H␈↓functional equation to represent it in first order logic.  The functional equation is

␈↓ ↓H␈↓L17:    ␈↓↓∀x y.(x subexp y ≡ (x=y) ∨ ¬␈↓αat␈↓↓ y ∧ (x subexp ␈↓αa␈↓↓ y ∨ x subexp ␈↓αd␈↓↓ y))␈↓,
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 98


␈↓ ↓H␈↓␈↓ α_The␈α⊃axiom␈α⊃system␈α⊃consisting␈α⊂of␈α⊃L1-L17,␈α⊃B1-B12,␈α⊃and␈α⊂the␈α⊃sentences␈α⊃resulting␈α⊃from␈α⊂the
␈↓ ↓H␈↓schemata LS1 and LS2 will be called the axiom system Lisp1.

␈↓ ↓H␈↓␈↓ α_Starting␈αwith␈α␈↓↓subexp␈↓␈αand␈αthe␈αbasic␈αLisp␈αfunctions␈αand␈αpredicates␈αwe␈αwill␈αdefine␈αthree␈αother
␈↓ ↓H␈↓Lisp␈α⊃predicates␈α⊂without␈α⊃recursion.␈α⊂ By␈α⊃␈↓↓u istail v␈↓␈α⊂we␈α⊃mean␈α⊂that␈α⊃␈↓↓u␈↓␈α⊂can␈α⊃be␈α⊂obtained␈α⊃from␈α⊃␈↓↓v␈↓␈α⊂by
␈↓ ↓H␈↓repeated␈α␈↓↓cdr␈↓s.␈α Thus␈αthe␈αtails␈αof␈α(A␈α
B␈αC␈αD)␈αare␈α(A␈αB␈αC␈αD),␈α
(B␈αC␈αD),␈α(C␈αD),␈α(D)␈αand␈α
NIL.␈α The
␈↓ ↓H␈↓natural recursive definition of ␈↓↓istail␈↓ is

␈↓ ↓H␈↓3)␈↓ α8 ␈↓↓u istail v ← (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v)␈↓

␈↓ ↓H␈↓which according to the previous sections would lead to the first order formula

␈↓ ↓H␈↓4)␈↓ α8 ␈↓↓∀u v.(u istail v ≡ (u = v) ∨ (¬␈↓αn␈↓↓ v ∧ u istail ␈↓αd␈↓↓ v))␈↓,

␈↓ ↓H␈↓but␈α
(4)␈α
is␈α
still␈α
an␈αimplicit␈α
definition␈α
of␈α
␈↓↓istail␈↓,␈α
because␈αthe␈α
function␈α
being␈α
defined␈α
occurs␈α
on␈αboth
␈↓ ↓H␈↓sides of the equivalence sign.  A suitable explicit definition is

␈↓ ↓H␈↓5)␈↓ α8  ␈↓↓∀u v.(u istail v ≡ u subexp v ∧ ∀x.(u subexp x ∧ x subexp v ⊃ x = u ∨ u subexp ␈↓αd␈↓↓ x))␈↓.

␈↓ ↓H␈↓Next we shall define membership in a list.  We have

␈↓ ↓H␈↓6)␈↓ α8  ␈↓↓∀x v.(x ε v ≡ ∃u.(u istail v ∧ x = ␈↓αa␈↓↓ u))␈↓.

␈↓ ↓H␈↓Now we define an ␈↓↓a-list␈↓ - a familiar Lisp concept.  We have

␈↓ ↓H␈↓7)␈↓ α8  ␈↓↓∀w.(isalist w ≡ ∀x.(x ε w ⊃ ¬␈↓αat␈↓↓ x) ∧ ∀x1 x2.(x1 ε w ∧ x2 ε w ∧ ␈↓αa␈↓↓ x1 = ␈↓αa␈↓↓ x2 ⊃ x1 = x2))␈↓.

␈↓ ↓H␈↓Thus␈α∞an␈α
␈↓↓a-list␈↓␈α∞is␈α∞a␈α
list␈α∞of␈α
pairs␈α∞such␈α∞that␈α
no␈α∞S-expression␈α
is␈α∞the␈α∞first␈α
element␈α∞of␈α∞two␈α
different
␈↓ ↓H␈↓pairs.␈α⊃ Therefore,␈α⊃a-lists␈α⊃are␈α⊃suitable␈α⊃for␈α⊂representing␈α⊃finite␈α⊃lists␈α⊃of␈α⊃argument-value␈α⊃pairs␈α⊂for
␈↓ ↓H␈↓partial functions.

␈↓ ↓H␈↓␈↓ α_Finally,␈α
we␈α
need␈α
the␈α
familiar␈α
Lisp␈α
function␈α
␈↓↓assoc␈↓␈α
that␈α
is␈α
used␈α
for␈α
looking␈α
up␈α
atoms␈α
on␈α␈↓↓a-
␈↓ ↓H␈↓↓lists␈↓.  Its recursive definition is

␈↓ ↓H␈↓8)␈↓ α8  ␈↓↓assoc(x,w) ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ w ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ ␈↓αif␈↓↓ x = ␈↓αaa␈↓↓ w ␈↓αthen␈↓↓ ␈↓αa␈↓↓ w ␈↓αelse␈↓↓ assoc(x,␈↓αd␈↓↓ w)␈↓,

␈↓ ↓H␈↓which can be represented by

␈↓ ↓H␈↓9)␈↓ α8  ␈↓↓∀w x y.(x.y = assoc(x,w) ≡ ∃w1.(w1 istail w ∧ x.y = ␈↓αa␈↓↓ w1) ∨ assoc(x,w) = ␈↓NIL␈↓↓)␈↓.

␈↓ ↓H␈↓␈↓ α_Now let ␈↓↓f␈↓ be defined recursively by

␈↓ ↓H␈↓10)␈↓ α8  ␈↓↓f x ← ␈↓	t␈↓↓[f](x)␈↓.

␈↓ ↓H␈↓In␈α∂order␈α∞to␈α∂emphasize␈α∞the␈α∂parallel␈α∞between␈α∂a␈α∞partial␈α∂function␈α∞␈↓↓f␈↓␈α∂and␈α∞an␈α∂␈↓↓a-list␈↓␈α∞used␈α∂as␈α∂a␈α∞finite
␈↓ ↓H␈↓approximation, we define

␈↓ ↓H␈↓11)␈↓ α8 ␈↓	t␈↓↓'[w](x) = ␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(x,w) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(x,w)␈↓.

␈↓ ↓H␈↓␈↓ α_With this preparation we can write
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ 99


␈↓ ↓H␈↓12)␈↓ α8␈α
 ␈↓↓∀x␈α
y.(y␈α
=␈α
f(x)␈α
≡␈α
∃w.(x.y␈α∞=␈α
␈↓αa␈↓↓␈α
w␈α
∧␈α
∀x1␈α
y1␈α
w1.(w1␈α
istail␈α∞w␈α
∧␈α
x1.y1␈α
=␈α
␈↓αa␈↓↓␈α
w1␈α
⊃␈α
y1␈α∞=␈α
␈↓	t␈↓↓'[␈↓αd␈↓↓
␈↓ ↓H␈↓↓w1](x1))) ∨ f(x) = ␈↓	w␈↓↓)␈↓.

␈↓ ↓H␈↓␈↓ α_The␈α∞essence␈α
of␈α∞this␈α
formula␈α∞is␈α
simple.␈α∞ ␈↓↓w␈↓␈α
is␈α∞an␈α
a-list␈α∞containing␈α
all␈α∞argument-value␈α
pairs
␈↓ ↓H␈↓that␈α⊂arise␈α⊂in␈α⊂the␈α⊂evaluation␈α⊂of␈α⊂␈↓↓f(x).␈α⊂We␈↓␈α⊂require␈α⊂that␈α⊂if␈α⊂␈↓↓x␈↓␈α⊂occurs␈α⊂somewhere␈α⊂on␈α⊂␈↓↓w,␈↓␈α⊂the␈α∂pairs
␈↓ ↓H␈↓involved␈α∞in␈α∞the␈α∞evaluation␈α∂of␈α∞␈↓↓f(x)␈↓␈α∞occur␈α∞further␈α∂on␈α∞in␈α∞the␈α∞a-list␈α∂␈↓↓w.␈↓␈α∞ This␈α∞is␈α∞to␈α∂avoid␈α∞allowing
␈↓ ↓H␈↓circular recursions.  If there is no such a-list, then ␈↓↓f(x) = ␈↓	w␈↓.

␈↓ ↓H␈↓␈↓ α_If␈α
the␈αlogic␈α
has␈α
a␈αdescription␈α
operator␈α
␈↓	i␈↓,␈αwhere␈α
␈↓	i␈↓↓␈α
x.P(x)␈↓␈αstands␈α
for␈α
the␈α"the␈α
unique␈α
␈↓↓x␈↓␈αsuch
␈↓ ↓H␈↓that ␈↓↓P(x)␈↓ if there is such a unique ␈↓↓x␈↓ and otherwise ␈↓	w␈↓", then (12) can be written

␈↓ ↓H␈↓13)␈↓ α8␈α∂␈↓↓∀x.(f(x)␈α∂=␈α∂␈↓	i␈↓↓␈α∂y.∃w.(x.y␈α∂=␈α∂␈↓αa␈↓↓␈α∂w␈α∂∧␈α∂∀x1␈α∂y1␈α∂w1.(w1␈α∂istail␈α∂w␈α∂∧␈α∂x1.y1␈α∂=␈α∂␈↓αa␈↓↓␈α∂w1␈α∂⊃␈α∂y1␈α∂=␈α∂␈↓	t␈↓↓'[␈↓αd␈↓↓
␈↓ ↓H␈↓↓w1](x1))))␈↓.

␈↓ ↓H␈↓␈↓ α_As an example, consider the Lisp function ␈↓↓ff␈↓ defined recursively by

␈↓ ↓H␈↓14)␈↓ α8 ␈↓↓ff x ← ␈↓αif␈↓↓ ␈↓αat␈↓↓ x ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ ff ␈↓αa␈↓↓ x␈↓.

␈↓ ↓H␈↓(13) then takes the form

␈↓ ↓H␈↓15)␈↓ α8␈α
∀x.(ff␈α
x␈α=␈α
␈↓	i␈↓↓x.∃w.(x.y␈α
=␈α
␈↓αa␈↓↓␈αw␈α
∧␈α
∀x1␈αy1␈α
w1.(w1␈α
istail␈α
w␈α∧␈α
x1.y1␈α
=␈α␈↓αa␈↓↓␈α
w1␈α
⊃␈α
y1␈α=␈α
␈↓αif␈↓↓␈α
␈↓αat␈↓↓␈αx1␈α
␈↓αthen␈↓↓
␈↓ ↓H␈↓↓x1 ␈↓αelse␈↓↓ (␈↓αif␈↓↓ ␈↓αn␈↓↓ assoc(x1,w1) ␈↓αthen␈↓↓ ␈↓	w␈↓↓ ␈↓αelse␈↓↓ ␈↓αd␈↓↓ assoc(x1,w1)))))␈↓.

␈↓ ↓H␈↓␈↓ α_Suppose␈α∞we␈α∞were␈α∞computing␈α∞␈↓↓ff ((A.B).C)␈↓.␈α
 A␈α∞suitable␈α∞␈↓↓w␈↓␈α∞would␈α∞be␈α∞((((A.B).C).A)␈α
((A.B).A)
␈↓ ↓H␈↓(A.A)).

␈↓ ↓H␈↓␈↓ α_It␈α
might␈α∞be␈α
asked␈α
whether␈α∞␈↓↓subexp␈↓␈α
is␈α
necessary.␈α∞ Couldn't␈α
we␈α
represent␈α∞recursive␈α
programs
␈↓ ↓H␈↓using␈α
just␈α
␈↓↓car,␈α
cdr,␈α
cons␈↓␈αand␈α
␈↓↓atom␈↓?␈α
 No,␈α
because␈α
the␈αany␈α
sentence␈α
involving␈α
just␈α
these␈αfunctions␈α
is
␈↓ ↓H␈↓decideable,␈α∂because␈α∂any␈α∂such␈α⊂sentence␈α∂can␈α∂be␈α∂converted␈α∂to␈α⊂an␈α∂equivalent␈α∂sentence␈α∂in␈α⊂the␈α∂pure
␈↓ ↓H␈↓theory of equality.

␈↓ ↓H␈↓␈↓ α_In␈α∞case␈α∞of␈α∞functions␈α∞of␈α∞several␈α∞variables,␈α∞(12)␈α∞corresponds␈α∞to␈α∞a␈α∂call-by-value␈α∞computation
␈↓ ↓H␈↓rule␈αwhile␈αthe␈αrepresentations␈αof␈αthe␈αprevious␈αsections␈αcorrespond␈αto␈αcall-by-name␈αor␈αother␈α"safe"
␈↓ ↓H␈↓rules.


␈↓ ↓H␈↓α8. Questions of Incompleteness.

␈↓ ↓H␈↓␈↓ α_Luckham,␈αPark␈αand␈αPaterson␈α(1970)␈αhave␈αshown␈αthat␈αwhether␈αa␈αprogram␈α
schema␈αdiverges
␈↓ ↓H␈↓for␈α∞every␈α∞interpretation,␈α∂whether␈α∞it␈α∞diverges␈α∞for␈α∂some␈α∞interpretation,␈α∞and␈α∞whether␈α∂two␈α∞program
␈↓ ↓H␈↓schemas␈α∀are␈α∪equivalent␈α∀are␈α∀all␈α∪not␈α∀even␈α∪partially␈α∀solvable␈α∀problems.␈α∪ Manna␈α∀(1974)␈α∀has␈α∪a
␈↓ ↓H␈↓thorough␈αdiscussion␈αof␈αthese␈αpoints.␈α In␈αview␈αof␈αthese␈αresults,␈αwhat␈αcan␈αbe␈αexpected␈αfrom␈αour␈αfirst
␈↓ ↓H␈↓order representations?

␈↓ ↓H␈↓␈↓ α_First␈α
let␈α
us␈α
construct␈α
a␈α
Lisp␈α
computation␈α
that␈α
does␈α
not␈α
terminate,␈α
but␈α
whose␈α
non-termination
␈↓ ↓H␈↓cannot␈α
be␈α
proved␈α
from␈α
the␈αaxioms␈α
Lisp1␈α
within␈α
first␈α
order␈αlogic.␈α
 We␈α
need␈α
only␈α
program␈αa␈α
proof-
␈↓ ↓H␈↓checker␈α
for␈αfirst␈α
order␈α
logic,␈αset␈α
it␈α
to␈αgenerate␈α
all␈αpossible␈α
proofs␈α
starting␈αwith␈α
the␈α
axioms␈αLisp1,
␈↓ ↓H␈↓and␈α
stop␈α
when␈α
it␈αfinds␈α
a␈α
proof␈α
of␈α(NIL␈α
≠␈α
NIL)␈α
or␈αsome␈α
other␈α
contradiction.␈α
 Assuming␈αthe␈α
axioms
␈↓ ↓H␈↓are␈α
consistent,␈αthe␈α
program␈αwill␈α
never␈α
find␈αsuch␈α
a␈αproof␈α
and␈α
will␈αnever␈α
stop.␈α In␈α
fact,␈αproving␈α
that
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *10


␈↓ ↓H␈↓the␈α∂program␈α∂will␈α∂never␈α⊂stop␈α∂is␈α∂precisely␈α∂proving␈α∂that␈α⊂the␈α∂axioms␈α∂are␈α∂consistent.␈α⊂ But␈α∂Goedel's
␈↓ ↓H␈↓theorem␈α
asserts␈α
that␈α
axiom␈αsystems␈α
like␈α
Lisp1␈α
cannot␈αbe␈α
proved␈α
consistent␈α
within␈αthemselves.␈α
 The
␈↓ ↓H␈↓question␈αis␈αwhether␈αthis␈αis␈αthe␈αtypical␈αcase␈αof␈αa␈αcomputation␈αthat␈αcan't␈αbe␈αproved␈αnot␈αto␈αterminate
␈↓ ↓H␈↓or whether the system is too weak to prove the non-termination of more mundane computations.

␈↓ ↓H␈↓␈↓ α_We␈α
can␈α
presumably␈α
prove␈αLisp1␈α
consistent␈α
just␈α
as␈αGentzen␈α
proved␈α
arithmetic␈α
consistent␈α-␈α
at
␈↓ ↓H␈↓the␈α
price␈αof␈α
introducing␈α
a␈αnew␈α
axiom␈αschema␈α
that␈α
allows␈αinduction␈α
up␈αto␈α
the␈α
transfinite␈αordinal
␈↓ ↓H␈↓ε␈↓β0␈↓.  Proving the new system consistent will require induction up to a still higher ordinal, etc.

␈↓ ↓H␈↓␈↓ α_Since␈α∞every␈α∞recursively␈α∞defined␈α∞function␈α∞can␈α∞be␈α∞defined␈α∞explicitly,␈α∞any␈α∞sentence␈α
involving
␈↓ ↓H␈↓such␈α∂functions␈α∞can␈α∂be␈α∞replaced␈α∂by␈α∞an␈α∂equivalent␈α∞sentence␈α∂involving␈α∞only␈α∂␈↓↓subexp␈↓␈α∞and␈α∂the␈α∞basic
␈↓ ↓H␈↓Lisp␈α∞functions.␈α∞ The␈α∞theory␈α∞of␈α∞subexp␈α∞and␈α∞these␈α∞functions␈α∞has␈α∞a␈α∞standard␈α∞model,␈α∞the␈α∂usual␈α∞S-
␈↓ ↓H␈↓expressions␈α∞and␈α∞many␈α∂non-standard␈α∞models.␈α∞ We␈α∞"construct"␈α∂non-standard␈α∞models␈α∞in␈α∂the␈α∞usual
␈↓ ↓H␈↓way␈α
by␈αappealing␈α
to␈αthe␈α
theorem␈αthat␈α
if␈αevery␈α
finite␈αsubset␈α
of␈αa␈α
set␈α␈↓↓S␈↓␈α
of␈αsentences␈α
of␈α
first␈αorder
␈↓ ↓H␈↓logic␈αhas␈αa␈αmodel,␈αthen␈α␈↓↓S␈↓␈αhas␈αa␈αmodel.␈α For␈αexample,␈αtake␈α␈↓↓S␈α=␈α{␈↓NIL␈↓↓␈αsubexp␈αx,␈α␈↓(A)␈↓↓␈αsubexp␈αx,␈α␈↓(A
␈↓ ↓H␈↓A)␈↓↓␈α
subexp␈α
x,␈α
...␈↓␈α
indefinitely}.␈α
 Every␈α
finite␈α
subset␈α
of␈α
␈↓↓S␈↓␈α
has␈α
a␈α
model;␈α
we␈α
need␈α
only␈α
take␈α
␈↓↓x␈↓␈α
to␈α
be␈α
the
␈↓ ↓H␈↓longest␈αlist␈αof␈αA's␈α
occurring␈αin␈αthe␈αsentences.␈α Hence␈α
there␈αis␈αa␈αmodel␈α
of␈αthe␈αLisp␈αaxioms␈αin␈α
which
␈↓ ↓H␈↓␈↓↓x␈↓␈αhas␈αall␈αlists␈αof␈αA's␈αas␈αsubexpressions.␈α No␈αsentence␈αtrue␈αin␈αthe␈αstandard␈αmodel␈αand␈αfalse␈αin␈αsuch
␈↓ ↓H␈↓a␈α
model␈α
can␈α
be␈α
proved␈α
from␈α
the␈α
axioms.␈α
 However,␈α
it␈α
is␈α
necessary␈α
to␈α
be␈α
careful␈α
about␈αthe␈α
meaning
␈↓ ↓H␈↓of␈αtermination␈αof␈αa␈αfunction.␈α
 In␈αfact,␈αtaking␈αsuccessive␈α␈↓↓cdr␈↓s␈α
of␈αsuch␈αan␈α␈↓↓x␈↓␈αwould␈α
never␈αterminate,
␈↓ ↓H␈↓but␈α
the␈αsentence␈α
whose␈α␈↓↓standard␈α
interpretation␈↓␈αis␈α
termination␈αof␈α
the␈αcomputation␈α
is␈αprovable␈α
from
␈↓ ↓H␈↓Lisp1.

␈↓ ↓H␈↓␈↓ α_The␈α⊂practical␈α⊂question␈α∂is:␈α⊂where␈α⊂does␈α∂the␈α⊂correctness␈α⊂of␈α∂ordinary␈α⊂programs␈α⊂come␈α⊂in?␈α∂ It
␈↓ ↓H␈↓seems␈αlikely␈α
that␈αsuch␈α
statements␈αwill␈αbe␈α
provable␈αwith␈α
our␈αoriginal␈αsystem␈α
of␈αaxioms.␈α
 It␈αdoesn't
␈↓ ↓H␈↓follow␈α∞that␈α∞the␈α∞system␈α∂Lisp1␈α∞will␈α∞permit␈α∞convenient␈α∞proofs,␈α∂but␈α∞probably␈α∞it␈α∞will.␈α∂ The␈α∞heuristic
␈↓ ↓H␈↓evidence␈αfor␈αthis␈α
comes␈αfrom␈α(Cohen␈α
1965).␈α Cohen␈αpresents␈α
two␈αsystems␈αof␈αaxiomaized␈α
arithmetic
␈↓ ↓H␈↓Z1␈α
and␈α
Z2.␈α
 Z1␈α∞is␈α
ordinary␈α
Peano␈α
arithmetic␈α∞with␈α
an␈α
axiom␈α
schema␈α∞of␈α
induction,␈α
and␈α
Z2␈α∞is␈α
an
␈↓ ↓H␈↓axiomatization␈α
of␈αhereditarily␈α
finite␈α
sets␈αof␈α
integers.␈α Superficially,␈α
Z2␈α
is␈αmore␈α
powerful␈α
than␈αZ1,
␈↓ ↓H␈↓but␈α
because␈αthe␈α
set␈αoperations␈α
of␈α
Z2␈αcan␈α
be␈αrepresented␈α
in␈α
Z1␈αas␈α
functions␈αon␈α
the␈αGoedel␈α
numbers
␈↓ ↓H␈↓of␈α⊃the␈α⊃sets,␈α∩it␈α⊃turns␈α⊃out␈α∩that␈α⊃Z1␈α⊃is␈α⊃just␈α∩as␈α⊃powerful␈α⊃once␈α∩the␈α⊃necessary␈α⊃machinery␈α∩has␈α⊃been
␈↓ ↓H␈↓established.␈α Because␈αsets␈αand␈αlists␈αare␈αthe␈αbasic␈αdata␈αof␈αLisp1,␈αand␈αsets␈αare␈αeasily␈αrepresented,␈αthe
␈↓ ↓H␈↓power␈αof␈αLisp1␈αwill␈αbe␈αapproximately␈αthat␈αof␈αZ2,␈αand␈αconvenient␈αproofs␈αof␈αcorrectness␈αstatements
␈↓ ↓H␈↓should be possible.  It would be nice to be able to express these considerations less vaguely.


␈↓ ↓H␈↓α9. References.

␈↓ ↓H␈↓␈↓αCartwright,␈αR.S.␈α(1977)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ ↓H␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ ↓H␈↓␈↓αCohen, Paul (1966)␈↓: ␈↓↓Set Theory and the Continuum Hypothesis␈↓, W.A. Benjamin Inc.

␈↓ ↓H␈↓␈↓αCooper,␈αD.C.␈α(1969)␈↓:␈α"Program␈αScheme␈αEquivalences␈αand␈αSecond-order␈αLogic",␈αin␈αB.␈αMeltzer␈αand
␈↓ ↓H␈↓D. Michie (eds.), ␈↓↓Machine Intelligence␈↓, Vol. 4, pp. 3-15, Edinburgh University Press, Edinburgh.

␈↓ ↓H␈↓␈↓αKleene, S.C. (1951)␈↓: ␈↓↓Introduction to Metamathematics␈↓, Van Nostrand, New York.

␈↓ ↓H␈↓␈↓αLuckham,␈αD.C.,␈αD.M.R.Park,␈α
and␈αM.S.␈αPaterson␈α(1970)␈↓:␈α
"On␈αFormalized␈αComputer␈αPrograms",␈α
␈↓↓J.
␈↓ ↓H␈↓↓CSS␈↓, ␈↓α4␈↓(3): 220-249 (June).
␈↓ ↓H␈↓REPRESENTATION␈↓ ε⊗...draft...␈↓ *11


␈↓ ↓H␈↓␈↓αManna,␈αZohar␈αand␈αAmir␈αPnueli␈α(1970)␈↓:␈α"Formalizatin␈αof␈αthe␈αProperties␈αof␈αFunctional␈αPrograms",
␈↓ ↓H␈↓␈↓↓J. ACM␈↓, ␈↓α17␈↓(3): 555-569.

␈↓ ↓H␈↓␈↓αManna, Zohar (1974)␈↓: ␈↓↓Mathematical Theory of Computation␈↓, McGraw-Hill.

␈↓ ↓H␈↓␈↓αManna,␈α∀Zohar,␈α∀Stephen␈α∀Ness␈α∀and␈α∀Jean␈α∀Vuillemin␈α∀(1973)␈↓:␈α∀"Inductive␈α∀Methods␈α∀for␈α∀Proving
␈↓ ↓H␈↓Properties of Programs", ␈↓↓Comm. ACM␈↓,␈↓α16␈↓(8): 491-502 (August).

␈↓ ↓H␈↓␈↓αMorris,␈α⊂James␈α⊂H.,␈α⊂and␈α∂Ben␈α⊂Wegbreit␈α⊂(1977)␈↓:␈α⊂"Program␈α∂Verification␈α⊂by␈α⊂Subgoal␈α⊂Induction",␈α∂to
␈↓ ↓H␈↓appear.

␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Artificial Intelligence Laboratory
␈↓ ↓H␈↓Computer Science Department
␈↓ ↓H␈↓Stanford University
␈↓ ↓H␈↓Stanford, California 94305

␈↓ ↓H␈↓ARPANET: MCCARTHY@SU-AI

␈↓ ↓H␈↓␈↓εThis draft of FIRST.NEW[W77,JMC] PUBbed at 1:13 on February 22, 1977.␈↓